|
In proof complexity, a Frege system is a propositional proof system whose proofs are sequences of formulas derived using a finite set of sound and implicationally complete inference rules. Frege systems (more often known as Hilbert systems in general proof theory) are named after Gottlob Frege. ==Formal definition== Let ''K'' be a finite functionally complete set of Boolean connectives, and consider propositional formulas built from variables ''p''0, ''p''1, ''p''2, ... using ''K''-connectives. A Frege rule is an inference rule of the form : where ''B''1, ..., ''Bn'', ''B'' are formulas. If ''R'' is a finite set of Frege rules, then ''F'' = (''K'',''R'') defines a derivation system in the following way. If ''X'' is a set of formulas, and ''A'' is a formula, then an ''F''-derivation of ''A'' from axioms ''X'' is a sequence of formulas ''A''1, ..., ''Am'' such that ''Am'' = ''A'', and every ''Ak'' is a member of ''X'', or it is derived from some of the formulas ''Ai'', ''i'' < ''k'', by a substitution instance of a rule from ''R''. An ''F''-proof of a formula ''A'' is an ''F''-derivation of ''A'' from the empty set of axioms (). ''F'' is called a Frege system if *''F'' is sound: every ''F''-provable formula is a tautology. *''F'' is implicationally complete: for every formula ''A'' and a set of formulas ''X'', if ''X'' entails ''A'', then there is an ''F''-derivation of ''A'' from ''X''. The length (number of lines) in a proof ''A''1, ..., ''Am'' is ''m''. The size of the proof is the total number of symbols. A derivation system ''F'' as above is refutationally complete, if for every inconsistent set of formulas ''X'', there is an ''F''-derivation of a fixed contradition from ''X''. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Frege system」の詳細全文を読む スポンサード リンク
|